a:rationals. ((a + -(a)) = 0  rationals)  ((-(a) + a) = 0  rationals) 

latex

Definitions	imon{i:l}, t  T, igrp{i:l}, t.2, t.1, prop{i:l}, mon{i:l}, grp{i:l}, abgrp{i:l}, qadd_grp, grp_id(g), grp_inv(g), grp_op(g), x f y, grp_car(g), P  Q, x:A. B(x)
Lemmas	abgrp wf, grp inv wf, inverse wf, grp id wf, grp op wf, grp car wf, monoid p wf, qadd grp wf, grp inverse